
package extensionTools.smvCreator;
//import java.util.Random;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Set;

import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvDBException;
import extensionTools.smvCreator.Link.LinkType;
import extensionTools.smvCreator.Link.SmvType;

/**
 * @author Dennis
 *
 */

public class EvCreate extends Rule {

	public EvCreate(DiagramDatabase db) {
		super(db);
	}

	/**
	 * This function receives a database and creates all of the the object
	 * creation event rules.
	 * The event rules include:
	 * 
	 * ev_create_processName_processInstance_objectName - selecting the instance of the object that
	 * 													  this process instance will create.
	 * 
	 * ev_create_processName_processInstance_objectName_objectInstance - an event for choosing the instance
	 * 												of object by this process with this instance
	 * 
	 * ev_create_processName_processInstance_objectName_objectInstance_stateName - the same as above
	 * 												only stateName tells us that the object have an
	 * 												initial state, and it will be created in this state
	 * 
	 * ev_create_objectName_objectInstance - event for creating a environmental object
	 * 
	 * @param db the system's Database
	 * @return A String in SMV which implements the event rules
	 * @throws RulesUtilsException 
	 * @throws SmvDBException 
	 */
	@Override
	public String createRule() throws RulesUtilsException, SmvDBException {
		ArrayList<SmvObject> objects = db.getSmvObjectList();
		String rule = "";
		for (SmvObject obj : objects) {	
			if(obj.isEnvironmental()){
				rule +="\n" + environmentalCreation(obj,db);
			}
			rule += "\n" + normalCreation(obj , db);
		}

		return rule;
	}
	
	/**
	 * This function creates the ev_create of an environmental object "ev_create_objectName_objectInstance"
	 * @param obj -The environmental object
	 * @param db - The diagram database
	 * @return A String in SMV which implements the rule
	 * @throws RulesUtilsException 
	 */
	private String environmentalCreation(SmvObject obj, DiagramDatabase db) throws RulesUtilsException {
		db.getCreationVar();
		
		RulesUtils.checkParamsForNull(obj,db);
		
		String name = "ev_create_"+obj.getName();
		String returnRule = "";
		for (int i=0;i<SMVCreator.K;i++)
		{
			String initialState = "";
			State  initState = obj.getInitialState();
			if (null != initState)
			{
				initialState = "_" + initState.getName();
			}

			String[] caseLines = new String[3];
			caseLines[0] = SmvOp.createCaseLine(SmvOp.and("sysState = event1",
              	  		obj.getName()+"_"+i+"=notExist"), 
              	  		SmvOp.prepareTerminationRes(db.getCreationVar()));
			caseLines[1] = SmvOp.createCaseLine(SmvOp.and("sysState = event2" 
												,"!("+obj.getName()+"_"+i+"=notExist)"),"1");
			caseLines[2] = SmvOp.createCaseLine ("TRUE", "1");
			returnRule += SmvOp.next(name+"_"+i+initialState,SmvOp.createCaseS(caseLines));
		}
		return returnRule;
	}

	/**
	 * This function creates the event rules regarding the creation with regular RESULT link (link not
	 * in XOR/OR) and the event rule regarding the instance of the object, that the process will create
	 * All of this is for non-environmental objects.
	 * 
	 * ev_create_processName_processInstance_objectName_objectInstance
	 * 				OR
	 * ev_create_processName_processInstance_objectName_objectInstance_initialState
	 * 
	 * ev_create_processName_processInstance_objectName
	 * 
	 * @param obj -The object
	 * @param db - The diagram database
	 * @return A String in SMV which implements the rule
	 * @throws RulesUtilsException 
	 * @throws SmvDBException 
	 */
	private String normalCreation(SmvObject obj, DiagramDatabase db) throws RulesUtilsException, SmvDBException {
		RulesUtils.checkParamsForNull(obj,db);
		String normalRule = "";
		//all the links that going out/to the object obj
		ArrayList<Link > objLinks = obj.getLinkList();
		for (Link lnk : objLinks) {		
			if (lnk.getLinkType() == LinkType.RESULT && lnk.getLabel().equals(""))
			{
				
				normalRule+=createProcessObject(obj,lnk,db);
			}				
		}		
		return normalRule;
}

	


	/**
	 * This function creates the event rules regarding the creation with regular RESULT link (link not
	 * in XOR/OR).
	 * 
	 * ev_create_processName_processInstance_objectName_objectInstance
	 * 				OR
	 * ev_create_processName_processInstance_objectName_objectInstance_initialState
	 * 
	 * @param obj -The object
	 * @param lnk -The link from a process to the object (obj). Object may have many links ,some of them
	 * 			   even a RESULT from other object, so we will create a separate rule.
	 * @param db - The diagram database
	 * @return A String in SMV which implements the rule
	 * @throws RulesUtilsException 
	 * @throws SmvDBException 
	 */
	private String createProcessObject(SmvObject obj, Link lnk, DiagramDatabase db) throws RulesUtilsException, SmvDBException {
		
		RulesUtils.checkParamsForNull(obj,db,lnk);
		
		String states ="";
		long dstId = lnk.getDstId();
		String objName = obj.getName();
		String returnRule ="";
		
		
		SmvType srcType = lnk.getSrcType();
		//we are looking for only links between process and object
		if(srcType != SmvType.PROCESS) return returnRule;
				
		//the object is the destination of the link
		if (dstId == obj.getId())
		{ 
			State  initState = obj.getInitialState();
			//no initial state so we will randomly pick the next state;
			if(initState == null && obj.getStateList().size() > 0){
				states =RulesUtils.getStateNames(obj);				
			}
			if (initState != null)
			{
				states = initState.getName();	
			}
		}
		//the destination is not an object
		else
		{
			//find if the link destination was one of the object states
			State dstState = obj.idBelongsToObj(dstId);
			if(null != dstState) 
			{
				states = dstState.getName();
			}
			else
			{
        		throw new SmvDBException("EvCreate: A link:"+ lnk + " " +
        				"that belongs to Object"+ obj.getName()
    				+"and her source is a process do not point to and Object " +
    						"or to one of its " +"states");
			}
		}
	String firstState = "_"+states;
	
	if (states.endsWith("notExist")|| states == "")
	{
		firstState="";
	}
	int k = SMVCreator.K;
	for (int i=0; i<k; i++){		
		String processName = db.getProcessNameById(lnk.getSrcId());
		returnRule  += evCreateNoStates(objName, processName, firstState,"TRUE","FALSE","event2","event2",i);
		returnRule += evCreatePhase(objName,firstState, processName,"phase1","event1",i);
		

	}

		return returnRule;
}


	
    /**
     * This function create the next case line for ev_create_process_i_obj. it will randomize the instance from the 
     * free instances (the ones that are being used)
     * @param objName - the object name
     * @param initialState - object initial State
     * @param procName - the process name
     * @param sysStateTrue - the system state for turning on the ev_create
     * @param sysStateTrue - the system state for turning off the ev_create
     * @return A string that hold the next for this ev_create
     * @throws RulesUtilsException 
     */
	private String evCreatePhase(String currObjName, String initialState,
			String procName, String sysStateTrue, String sysStateFalse,int place)
			throws RulesUtilsException {
		

		Set<Integer> mySet = new HashSet<Integer>();

		int k = SMVCreator.K;
		//will create all object name permutation (power set) of a given length, going from k-1 to 1
		//this will build the case line for all the instances of the object that were already
		//created, so the current object will choose only from the available instances
		for (int i = k-1; i>=0;i--)
		{
			mySet.add(i);
		}

		String proccTerm = "ev_terminate_"+procName+"_";
		String finalRules ="";

		String objectLine = "";
		
		LinkedList<Set<Integer>> list = new LinkedList<Set<Integer>>();
	
		//Power set of all instances
		for (Set<Integer> s : RulesUtils.powerSet(mySet)) {
		     list.addFirst(s);
		 }
		
		ArrayList<String> usedObjects = new ArrayList<String>();
		//create all objectName_instance lines
		for (Set<Integer> s: list)
		{
			for (String objName_i : RulesUtils.nameAllObjectInstances(currObjName,s))
		     {
				objectLine=SmvOp.and(objectLine,"!("+objName_i+" = notExist)");
		     }
			Set<Integer> instance = RulesUtils.diffrenceSet(mySet,s);
			objectLine= SmvOp.createCaseLine(SmvOp.and("sysState = "+sysStateTrue,
					proccTerm+place+"=0",objectLine),createInstances(instance));
			usedObjects.add(objectLine);
			objectLine="";
		}
		//by sorting by size we will cover all options of taken objects, where the
		//longest lines are the lines where many of the objects are taken
		//think of it as a firewall configuration, if A is a subset of B
		//and A is the free objects, then A should come before B
		RulesUtils.sortBySize(usedObjects);
		
		String reset ="";
		//add the reset and default states
		for (int i=0; i<k; i++)
		{
			reset = SmvOp.createCaseLine(SmvOp.and("sysState = "+sysStateFalse,
					"ev_create_"+procName+"_"+place+"_"+currObjName+initialState+"="+i,
					currObjName+"_"+i+"=notExist"), 
					"false");
			usedObjects.add(usedObjects.size(), reset);
		}
		

		reset = SmvOp.createCaseLine(
				"TRUE", "ev_create_"+procName+"_"+place+"_"+currObjName+initialState);
		usedObjects.add(usedObjects.size(), reset);

		finalRules = SmvOp.next("ev_create_"+procName+"_"+place+"_"+currObjName+initialState,
				SmvOp.createCase(RulesUtils.arrayListToArray(usedObjects)) );
		
		return finalRules;
	}
		


   //
    /* This function create the values of all ev_create_proc_i_obj
    * @param instance - all the available instances numbers surrounded by brackets
    * @return A string with all instances {1,2,3,...n}
    * @throws RulesUtilsException - For null check
    */
	@SuppressWarnings("unchecked")
	private String createInstances(Set<Integer> instance) throws RulesUtilsException {
	
		RulesUtils.checkParamsForNull(instance);

		//the default is false
		String inst = "false";
		int size = instance.size();
		
		if (size == 0)
		{
			return inst;
		}
		ArrayList<Integer> instances = new ArrayList<Integer>(instance);
		String ins = instances.toString();
		ins = ins.substring(1, ins.length()-1);
		//if size = 1 then no brackets is needed
		if (ins.length() > 1)
		{
			 ins = "{"+ins+"}";
		}
		return ins;
}


    /**
     * This function create the next case line for ev_create_process_i_obj_j
     * @param objName - the object name
     * @param procName - the process name
     * @param states - if the process create the object with sates this will hold the states
     * 				   possibilities, only if the process point on a specific state
     * 				   we will create instead of ev_create_process_i_obj_j, 
     * 				   ev_create_process_i_obj_j_StateName
     * @param nextTrue  - what it should be if all the terms will be true
     * @param nextFalse  - what it should be if one of the terms for reseting this ev_create are true
     * @param sysStateTrue - the system state for turning on the ev_create
     * @param sysStateTrue - the system state for turning off the ev_create
     * @param place - the object permutation in k, (will be the j in obj_j)
     * @param k - the k of this system
     * @return A string that hold the next for this ev_create
     * @throws RulesUtilsException - when null parameters were sent to SmvOp
     */
	private String evCreateNoStates(String objName, 
								String procName,String firstState,String nextTrue, String nextFalse,  
								String sysStateTrue, String sysStateFalse,int place) throws RulesUtilsException {
		
		String currObjName = objName +"_"+ place;
		String proccTerm = "ev_terminate_"+procName+"_";
		String finalRules ="";

		//building this case line for example place=6: obj6=notExist & obj5=Exist & ... & obj0=Exist
		String preObjects = currObjName+"=notExist";


		int k = SMVCreator.K;
		for (int j=0 ; j<k; j++){
			String caseExist = SmvOp.createCaseLine(SmvOp.and("sysState = "+sysStateTrue,
					proccTerm+j+"=0"
					,preObjects, "ev_create_"+procName+"_"+j+"_"+objName+firstState+"="+ place)
					, nextTrue);
			String caseNotExist2 = SmvOp.createCaseLine(
				"TRUE", "ev_create_"+procName+"_"+j+"_"+currObjName+firstState);
			String caseNotExist1 = SmvOp.createCaseLine(
					"sysState ="+ sysStateFalse, nextFalse);

			finalRules += SmvOp.next("ev_create_"+procName+"_"+j+"_"+currObjName+firstState,
					SmvOp.createCaseS(caseExist,caseNotExist1,caseNotExist2) );
			
			
		}

		return finalRules;
	}
		



}

